M:MsgA, k:Knd, x:Id. M.aframe(k affects x)  Prop 

latex

Definitions	Knd, t  T, Id, type List, x.A(x), x:A. B(x), x. t(x), Top, a:A fp B(a), x:AB(x), KindDeq, x  dom(f), b, Type, {x:A| B(x) }, IdDeq, deq-member(eq;x;L), Prop, x,y. t(x;y), z != f(x)  P(a;z), M.aframe(k affects x), x:AB(x), MsgA
Lemmas	msga wf, fpf-val wf, deq-member wf, id-deq wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Id wf, Knd wf